$\forall$$n$:$\mathbb{N}$, $T$:Type, $R$:($T$$\rightarrow$$T$$\rightarrow$Prop), $x$, $y$:$T$.
\\[0ex]($x$ rel\_exp($T$;$R$;$n$) $y$) $\Leftrightarrow$ ($\exists$$z$:$T$. 0$<$$n$ \& ($x$ rel\_exp($T$;$R$;$n$$-$1) $z$) \& ($z$ $R$ $y$)) $\vee$ $n$ $=$ 0 $\in$ $\mathbb{Z}$ \& $x$ $=$ $y$